YES 31.299 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule Main
  ((readOct :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Lambda Reductions:
The following Lambda expression
\ndn * radix + d

is transformed to
readInt0 radix n d = n * radix + d

The following Lambda expression
\vu77
case vu77 of
 (ds,r) → (foldl1 (readInt0 radix) (map (fromIntegral . digToIntds),r: []
 _ → []

is transformed to
readInt1 radix digToInt vu77 = 
case vu77 of
 (ds,r) → (foldl1 (readInt0 radix) (map (fromIntegral . digToIntds),r: []
 _ → []

The following Lambda expression
\dfromEnum d - fromEnum_0

is transformed to
readOct0 d = fromEnum d - fromEnum_0

The following Lambda expression
\vu68
case vu68 of
 (cs@(_ : _),t) → (cs,t: []
 _ → []

is transformed to
nonnull0 vu68 = 
case vu68 of
 (cs@(_ : _),t) → (cs,t: []
 _ → []

The following Lambda expression
\(_,zs)→zs

is transformed to
zs0 (_,zs) = zs

The following Lambda expression
\(ys,_)→ys

is transformed to
ys0 (ys,_) = ys



↳ HASKELL
  ↳ LR
HASKELL
      ↳ CR

mainModule Main
  ((readOct :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Case Reductions:
The following Case expression
case vu77 of
 (ds,r) → (foldl1 (readInt0 radix) (map (fromIntegral . digToIntds),r: []
 _ → []

is transformed to
readInt10 radix digToInt (ds,r) = (foldl1 (readInt0 radix) (map (fromIntegral . digToIntds),r: []
readInt10 radix digToInt _ = []

The following Case expression
case vu68 of
 (cs@(_ : _),t) → (cs,t: []
 _ → []

is transformed to
nonnull00 (cs@(_ : _),t) = (cs,t: []
nonnull00 _ = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
HASKELL
          ↳ BR

mainModule Main
  ((readOct :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
cs@(vy : vz)

is replaced by the following term
vy : vz

The bind variable of the following binding Pattern
xs@(ww : wx)

is replaced by the following term
ww : wx



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
HASKELL
              ↳ COR

mainModule Main
  ((readOct :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
span p [] = ([],[])
span p (ww : wx)
 | p ww
 = (ww : ys,zs)
 | otherwise
 = ([],ww : wx)
where 
vu43  = span p wx
ys  = ys0 vu43
ys0 (ys,wy) = ys
zs  = zs0 vu43
zs0 (wz,zs) = zs

is transformed to
span p [] = span3 p []
span p (ww : wx) = span2 p (ww : wx)

span2 p (ww : wx) = 
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys0 vu43
ys0 (ys,wy) = ys
zs  = zs0 vu43
zs0 (wz,zs) = zs

span3 p [] = ([],[])
span3 xx xy = span2 xx xy



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
HASKELL
                  ↳ LetRed

mainModule Main
  ((readOct :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys0 vu43
ys0 (ys,wy) = ys
zs  = zs0 vu43
zs0 (wz,zs) = zs

are unpacked to the following functions on top level
span2Zs0 xz yu (wz,zs) = zs

span2Span0 xz yu p ww wx True = ([],ww : wx)

span2Ys xz yu = span2Ys0 xz yu (span2Vu43 xz yu)

span2Vu43 xz yu = span xz yu

span2Zs xz yu = span2Zs0 xz yu (span2Vu43 xz yu)

span2Ys0 xz yu (ys,wy) = ys

span2Span1 xz yu p ww wx True = (ww : span2Ys xz yu,span2Zs xz yu)
span2Span1 xz yu p ww wx False = span2Span0 xz yu p ww wx otherwise



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
HASKELL
                      ↳ NumRed

mainModule Main
  ((readOct :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
HASKELL
                          ↳ Narrow

mainModule Main
  (readOct :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs(:(yv70, yv71), yv8) → new_psPs(yv71, yv8)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Zs0(Char(Succ(yv8500)), yv86, yv87, yv88) → new_span2Zs00(yv8500, yv86, yv8500, yv87, yv88)
new_span2Zs00(yv107, yv108, Succ(yv1090), Zero, yv111) → new_span2Zs01(yv107, yv108, Succ(yv107), Succ(yv111))
new_span2Zs01(yv128, yv129, Zero, Zero) → new_span2Zs03(yv128, yv129)
new_span2Zs(:(yv660, yv661)) → new_span2Zs0(yv660, yv661, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))
new_span2Zs02(yv107, yv108, yv111) → new_span2Zs01(yv107, yv108, Succ(yv107), Succ(yv111))
new_span2Zs01(yv128, yv129, Succ(yv1300), Succ(yv1310)) → new_span2Zs01(yv128, yv129, yv1300, yv1310)
new_span2Zs00(yv107, yv108, Zero, Zero, yv111) → new_span2Zs02(yv107, yv108, yv111)
new_span2Zs01(yv128, yv129, Zero, Succ(yv1310)) → new_span2Zs(yv129)
new_span2Zs00(yv107, yv108, Succ(yv1090), Succ(yv1100), yv111) → new_span2Zs00(yv107, yv108, yv1090, yv1100, yv111)
new_span2Zs03(yv128, yv129) → new_span2Zs(yv129)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(yv1040), Succ(yv1050)) → new_primMinusNat(yv1040, yv1050)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yv2130), Succ(yv19700)) → new_primPlusNat(yv2130, yv19700)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yv19100), yv190) → new_primMulNat(yv19100, yv190)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldl(yv160, yv161, yv162, yv163, Succ(yv1640), Zero, yv166, ba) → new_foldl0(yv160, yv161, yv162, yv163, Succ(yv162), Succ(yv166), ba)
new_foldl2(yv190, yv191, yv192, yv193, yv196, bb) → new_foldl4(yv190, yv191, new_pt(yv192, bb), yv193, bb)
new_foldl(yv160, yv161, yv162, yv163, Succ(yv1640), Succ(yv1650), yv166, ba) → new_foldl(yv160, yv161, yv162, yv163, yv1640, yv1650, yv166, ba)
new_foldl(yv160, yv161, yv162, yv163, Zero, Zero, yv166, ba) → new_foldl1(yv160, yv161, yv162, yv163, yv166, ba)
new_foldl6(yv147, yv154, Char(Succ(yv15000)), yv151, yv152, yv153, bd) → new_foldl(yv147, yv154, yv15000, yv151, yv15000, yv152, yv153, bd)
new_foldl1(yv160, yv161, yv162, yv163, yv166, ba) → new_foldl0(yv160, yv161, yv162, yv163, Succ(yv162), Succ(yv166), ba)
new_foldl3(yv190, yv191, yv192, yv193, bb) → new_foldl2(yv190, yv191, yv192, yv193, new_span2Zs1(yv193), bb)
new_foldl5(yv206, yv207, yv208, yv209, yv210, yv211, yv212, bc) → new_foldl6(yv206, new_readInt0(yv206, yv207, yv208, bc), yv209, yv210, yv211, yv212, bc)
new_foldl0(yv190, yv191, yv192, yv193, Zero, Succ(yv1950), bb) → new_foldl2(yv190, yv191, yv192, yv193, new_span2Zs1(yv193), bb)
new_foldl0(yv190, yv191, yv192, yv193, Succ(yv1940), Succ(yv1950), bb) → new_foldl0(yv190, yv191, yv192, yv193, yv1940, yv1950, bb)
new_foldl4(yv190, yv191, yv197, :(yv1930, yv1931), bb) → new_foldl5(yv190, yv191, yv197, yv1930, yv1931, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))), bb)
new_foldl0(yv190, yv191, yv192, yv193, Zero, Zero, bb) → new_foldl3(yv190, yv191, yv192, yv193, bb)

The TRS R consists of the following rules:

new_span2Zs1(:(yv660, yv661)) → new_span2Zs05(yv660, yv661, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))
new_span2Zs09(yv128, yv129) → new_span2Zs04(yv128, yv129, new_span2Zs1(yv129))
new_readInt0(yv190, Neg(yv1910), Neg(yv1970), ty_Int) → Neg(new_primPlusNat0(new_primMulNat0(yv1910, yv190), yv1970))
new_span2Zs06(yv107, yv108, Succ(yv1090), Zero, yv111) → new_span2Zs010(yv107, yv108, yv111)
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_pt(yv76, ty_Int) → new_primMinusInt(yv76, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))))
new_span2Zs010(yv107, yv108, yv111) → new_span2Zs08(yv107, yv108, Succ(yv107), Succ(yv111))
new_primMulNat0(Succ(yv19100), yv190) → new_primPlusNat0(new_primMulNat0(yv19100, yv190), Succ(yv190))
new_primMulNat0(Zero, yv190) → Zero
new_span2Zs04(yv128, yv129, yv133) → yv133
new_primMinusNat0(Zero, Succ(yv1050)) → Neg(Succ(yv1050))
new_primPlusNat0(Succ(yv2130), Succ(yv19700)) → Succ(Succ(new_primPlusNat0(yv2130, yv19700)))
new_primMinusInt(yv104, yv105) → new_primMinusNat0(yv104, yv105)
new_span2Zs08(yv128, yv129, Succ(yv1300), Succ(yv1310)) → new_span2Zs08(yv128, yv129, yv1300, yv1310)
new_span2Zs06(yv107, yv108, Zero, Succ(yv1100), yv111) → new_span2Zs07(yv107, yv108)
new_readInt0(yv190, Pos(yv1910), Neg(yv1970), ty_Int) → new_primMinusNat0(new_primMulNat0(yv1910, yv190), yv1970)
new_readInt0(yv190, Neg(yv1910), Pos(yv1970), ty_Int) → new_primMinusNat0(yv1970, new_primMulNat0(yv1910, yv190))
new_span2Zs07(yv107, yv108) → :(Char(Succ(yv107)), yv108)
new_primPlusNat0(Zero, Zero) → Zero
new_span2Zs1([]) → []
new_readInt0(yv190, Pos(yv1910), Pos(yv1970), ty_Int) → Pos(new_primPlusNat0(new_primMulNat0(yv1910, yv190), yv1970))
new_span2Zs06(yv107, yv108, Zero, Zero, yv111) → new_span2Zs010(yv107, yv108, yv111)
new_span2Zs08(yv128, yv129, Succ(yv1300), Zero) → new_span2Zs07(yv128, yv129)
new_span2Zs08(yv128, yv129, Zero, Zero) → new_span2Zs09(yv128, yv129)
new_pt(yv76, ty_Integer) → error([])
new_span2Zs06(yv107, yv108, Succ(yv1090), Succ(yv1100), yv111) → new_span2Zs06(yv107, yv108, yv1090, yv1100, yv111)
new_span2Zs05(Char(Succ(yv8500)), yv86, yv87, yv88) → new_span2Zs06(yv8500, yv86, yv8500, yv87, yv88)
new_readInt0(yv190, yv191, yv197, ty_Integer) → error([])
new_primMinusNat0(Succ(yv1040), Zero) → Pos(Succ(yv1040))
new_span2Zs08(yv128, yv129, Zero, Succ(yv1310)) → new_span2Zs09(yv128, yv129)
new_span2Zs05(Char(Zero), yv86, yv87, yv88) → :(Char(Zero), yv86)
new_primPlusNat0(Zero, Succ(yv19700)) → Succ(yv19700)
new_primPlusNat0(Succ(yv2130), Zero) → Succ(yv2130)
new_primMinusNat0(Succ(yv1040), Succ(yv1050)) → new_primMinusNat0(yv1040, yv1050)

The set Q consists of the following terms:

new_primMinusInt(x0, x1)
new_primMinusNat0(Succ(x0), Succ(x1))
new_span2Zs05(Char(Zero), x0, x1, x2)
new_span2Zs06(x0, x1, Zero, Succ(x2), x3)
new_readInt0(x0, Pos(x1), Pos(x2), ty_Int)
new_span2Zs04(x0, x1, x2)
new_pt(x0, ty_Int)
new_readInt0(x0, Neg(x1), Neg(x2), ty_Int)
new_primPlusNat0(Succ(x0), Zero)
new_span2Zs05(Char(Succ(x0)), x1, x2, x3)
new_pt(x0, ty_Integer)
new_span2Zs1(:(x0, x1))
new_span2Zs06(x0, x1, Succ(x2), Succ(x3), x4)
new_span2Zs08(x0, x1, Succ(x2), Succ(x3))
new_span2Zs07(x0, x1)
new_primMinusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_span2Zs1([])
new_primMinusNat0(Succ(x0), Zero)
new_span2Zs08(x0, x1, Succ(x2), Zero)
new_primMulNat0(Succ(x0), x1)
new_readInt0(x0, x1, x2, ty_Integer)
new_span2Zs06(x0, x1, Zero, Zero, x2)
new_span2Zs010(x0, x1, x2)
new_span2Zs08(x0, x1, Zero, Succ(x2))
new_span2Zs06(x0, x1, Succ(x2), Zero, x3)
new_primMulNat0(Zero, x0)
new_span2Zs08(x0, x1, Zero, Zero)
new_span2Zs09(x0, x1)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMinusNat0(Zero, Succ(x0))
new_readInt0(x0, Neg(x1), Pos(x2), ty_Int)
new_readInt0(x0, Pos(x1), Neg(x2), ty_Int)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_psPs0(:(yv720, yv721), yv73, ba) → new_psPs0(yv721, yv73, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: